Knaster Tarski Fixed Point Theorem
F-Consistent (F で 整合的) というのは x が F(x) よりも "小さい" (x <= F(x)) ってこと
そのような x の中で一番でっけえやつをとってきても、F(x) より小さいのはそれはそうなんだけど
この定理は驚くことに、一番でかいやつをもってくるとそれは F(x) と同じ (つまり x は F の fixed point ということ)
それもそのはず、考えているのは完備束なので、一番でかいやつってのは(Fで整合的な部分集合の)least upper boundがあるわけで。でかい x を F で移すと、
Fで整合的なので x <= F(x) だが
Fで整合的な部分集合を、Fで整合的な部分集合にうつしてるわけで、これ以上Fによってleast upper boundをでかくできない、
つまりFで整合的な部分集合のleast upper boundをFで移すともう天井突破できないので、それは同じくleast upper bound
またTaPL21章の文脈では、普遍集合の部分集合(集合一般)と包含関係が完備束になることを前提として話している
Knaster-Tarski Fixed point theorem は Complete Partial Ordered Set でも成り立つらしいぞ!(魔剤?)